the_w:World, i:Id, a:Action(i), l:IdLnk. (isrcv(l;a))  (msg(a)  Msg) 

latex

Definitions	x:A. B(x), P  Q, t  T, msg(a), b, isrcv(l;a), p  q, b, tt, if b then t else f fi , ff, , Msg, isrcv(k), lnk(k), tag(k), valtype(i;a), kindcase(k; a.f(a); l,t.g(l;t) ), t.1, outl(x), isl(x), islocal(k), act(k), t.2, outr(x), , Unit, P  Q, P & Q, False, Knd, , locl(a), rcv(l,tg)
Lemmas	assert wf, w-isrcvl wf, IdLnk wf, w-action wf, Id wf, world wf, w-isnull wf, bool wf, eqtt to assert, false wf, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, isrcv wf, w-kind wf, msg wf, w-M wf, lnk wf, tagof wf, w-val wf, Knd wf, subtype rel self, true wf